So, actually the title I should have edited,

I will correct it later, it should be

fairness and extensions of CTL,

fairness and CTL star, we will see why.

So, aha.

Okay, this is going to be a problem.

If it repeats in one more slide,

I'll try to adjust the projector again.

So,

what is going on here?

Why is it cut off?

How does it even communicate with it?

Okay, let's agree to screen again.

And does it say no?

No.

No.

Maybe this is actually too big a slide, sorry.

Well, fortunately, we have introduced

this definition last time, but I will then say that out.

Okay, at least I know that there is nothing wrong

with the full screen mode itself.

So, last time we discussed several types of

fairness constraints that one may be interested

in expressing in CTL.

Strong fairness, weak fairness,

and unconditional fairness.

Actually, the last one is easiest.

It's just of the form,

psi occurs infinity of around the path.

In slightly more general setup,

you could also allow conjunctions of conditions

of this form.

So, we can say that we want the path where psi one

occurs infinity often and psi two occurs infinitely often.

Notice, of course, that this is not the same thing as,

so, gf psi one and gf psi two

and gf psi two are not equivalent

to gf psi one and psi two.

Why?

Is it clear that they are not equivalent?

I should have actually stated it as a quiz.

Are they equivalent or not?

But now that you got the answer.

So, what we could always do is to pull this g

out of, in front of the conjunction

because g being universal quantifier like,

remember that g means for all points on the path.

So, now we are in LTL by the way, not in CTL.

But today, later I will introduce a setup

where you can write both path and state formulas